//===-- ExecutorUtil.cpp --------------------------------------------------===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//

#include "klee/Executor.h"

#include "klee/Context.h"

#include "klee/Expr.h"
#include "klee/Interpreter.h"
#include "klee/Solver.h"

#include "klee/Internal/Module/KModule.h"

#include "llvm/IR/Constants.h"
#include "llvm/IR/Function.h"
#include "llvm/IR/Instructions.h"
#include "llvm/IR/Module.h"
#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
#include "llvm/ModuleProvider.h"
#endif
#include <cassert>
#include <iostream>
#include "llvm/IR/CallSite.h"
#include "llvm/IR/DataLayout.h"
#include "llvm/IR/GetElementPtrTypeIterator.h"

using namespace klee;
using namespace llvm;

namespace klee {

ref<ConstantExpr> Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
    llvm::Type *type = ce->getType();

    ref<ConstantExpr> op1(0), op2(0), op3(0);
    int numOperands = ce->getNumOperands();

    if (numOperands > 0)
        op1 = evalConstant(ce->getOperand(0));
    if (numOperands > 1)
        op2 = evalConstant(ce->getOperand(1));
    if (numOperands > 2)
        op3 = evalConstant(ce->getOperand(2));

    switch (ce->getOpcode()) {
        default:
            ce->dump();
            std::cerr << "error: unknown ConstantExpr type\n"
                      << "opcode: " << ce->getOpcode() << "\n";
            abort();

        case Instruction::Trunc:
            return op1->Extract(0, getWidthForLLVMType(type));
        case Instruction::ZExt:
            return op1->ZExt(getWidthForLLVMType(type));
        case Instruction::SExt:
            return op1->SExt(getWidthForLLVMType(type));
        case Instruction::Add:
            return op1->Add(op2);
        case Instruction::Sub:
            return op1->Sub(op2);
        case Instruction::Mul:
            return op1->Mul(op2);
        case Instruction::SDiv:
            return op1->SDiv(op2);
        case Instruction::UDiv:
            return op1->UDiv(op2);
        case Instruction::SRem:
            return op1->SRem(op2);
        case Instruction::URem:
            return op1->URem(op2);
        case Instruction::And:
            return op1->And(op2);
        case Instruction::Or:
            return op1->Or(op2);
        case Instruction::Xor:
            return op1->Xor(op2);
        case Instruction::Shl:
            return op1->Shl(op2);
        case Instruction::LShr:
            return op1->LShr(op2);
        case Instruction::AShr:
            return op1->AShr(op2);
        case Instruction::BitCast:
            return op1;

        case Instruction::IntToPtr:
            return op1->ZExt(getWidthForLLVMType(type));

        case Instruction::PtrToInt:
            return op1->ZExt(getWidthForLLVMType(type));

        case Instruction::GetElementPtr: {
            ref<ConstantExpr> base = op1->ZExt(Context::get().getPointerWidth());

            for (gep_type_iterator ii = gep_type_begin(ce), ie = gep_type_end(ce); ii != ie; ++ii) {
                ref<ConstantExpr> addend = ConstantExpr::alloc(0, Context::get().getPointerWidth());

                if (StructType *st1 = dyn_cast<StructType>(*ii)) {
                    const StructLayout *sl = kmodule->dataLayout->getStructLayout(st1);
                    const ConstantInt *ci = cast<ConstantInt>(ii.getOperand());

                    addend = ConstantExpr::alloc(sl->getElementOffset((unsigned) ci->getZExtValue()),
                                                 Context::get().getPointerWidth());
                } else {
                    SequentialType *st = cast<SequentialType>(*ii);
                    ref<ConstantExpr> index = evalConstant(cast<Constant>(ii.getOperand()));
                    unsigned elementSize = kmodule->dataLayout->getTypeStoreSize(st->getElementType());

                    index = index->ZExt(Context::get().getPointerWidth());
                    addend = index->Mul(ConstantExpr::alloc(elementSize, Context::get().getPointerWidth()));
                }

                base = base->Add(addend);
            }

            return base;
        }

        case Instruction::ICmp: {
            switch (ce->getPredicate()) {
                default:
                    pabort("unhandled ICmp predicate");
                case ICmpInst::ICMP_EQ:
                    return op1->Eq(op2);
                case ICmpInst::ICMP_NE:
                    return op1->Ne(op2);
                case ICmpInst::ICMP_UGT:
                    return op1->Ugt(op2);
                case ICmpInst::ICMP_UGE:
                    return op1->Uge(op2);
                case ICmpInst::ICMP_ULT:
                    return op1->Ult(op2);
                case ICmpInst::ICMP_ULE:
                    return op1->Ule(op2);
                case ICmpInst::ICMP_SGT:
                    return op1->Sgt(op2);
                case ICmpInst::ICMP_SGE:
                    return op1->Sge(op2);
                case ICmpInst::ICMP_SLT:
                    return op1->Slt(op2);
                case ICmpInst::ICMP_SLE:
                    return op1->Sle(op2);
            }
        }

        case Instruction::Select:
            return op1->isTrue() ? op2 : op3;

        case Instruction::FAdd:
        case Instruction::FSub:
        case Instruction::FMul:
        case Instruction::FDiv:
        case Instruction::FRem:
        case Instruction::FPTrunc:
        case Instruction::FPExt:
        case Instruction::UIToFP:
        case Instruction::SIToFP:
        case Instruction::FPToUI:
        case Instruction::FPToSI:
        case Instruction::FCmp:
            pabort("floating point ConstantExprs unsupported");
    }
}
}
